eq\_seq(${\it eq}$)($s_{1}$,$s_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$s_{1}$/$k_{1}$,$g_{1}$. $s_{2}$/$k_{2}$,$g_{2}$. $k_{1}$=$_{2}$$k_{2}$ $\wedge_{2}$ primrec($k_{1}$;true$_{2}$;$\lambda$$i$,$b$. ${\it eq}$($g_{1}$($i$),$g_{2}$($i$)) $\wedge_{2}$ $b$)